$\forall$$A$:Type, $x$:($A$ + Top), $a$:Atom1. $x$:$A$ + Top$\parallel$$a$ $\Rightarrow$ ($\uparrow$isl($x$)) $\Rightarrow$ outl($x$):$A$$\parallel$$a$